a:, n:. Div(a;n;a  n) 

latex

Up	int 2, int 2
Definitions	t  T, Div(a;n;q), x:A. B(x), False, A, a  b  T , P  Q, P  Q, P & Q, T, P  Q, , True, i  j < k, A  B, {T}, , , S  T
Lemmas	nat wf, nat plus wf, rem bounds 1, nat plus inc int nzero, divide wfa, add mono wrt le rw, add mono wrt lt rw, div rem sum, add com, true wf, squash wf, le wf